A:Type, L:(A List). l_disjoint(A;L;[]) 

latex

Definitions	(x  l), Void, x:A  B(x), P & Q, x:AB(x), P  Q, False, A, Type, type List, t  T, s = t, , [], x:A. B(x), a < b, A c B, #$n, ||as||, A  B, , {x:A| B(x)} , , l[i], P  Q, P  Q, l_disjoint(T;l1;l2)
Lemmas	not functionality wrt iff, and functionality wrt iff, nil member, nat wf, length wf1, length wf2, select wf, l member wf, false wf